Appendix B in [Alpuente, Escobar and Lucas - RULE'03]

Summary: ExAppendixB_AEL03

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. Zantema's transformation (MetaCombination @ AProVE)
  2. Ferreira and Ribeiro's transformation (MetaCombination @ AProVE)
  3. Giesl and Middeldorp's transformation (Corollary)

CS-TRS ExAppendixB_AEL03 (file ExAppendixB_AEL03.csr)

Functions:  0 s posrecip negrecip nil cons cons2 rnil rcons from 2ndspos 2ndsneg pi plus times square

Constructors:  0 s posrecip negrecip nil cons cons2 rnil rcons

Variables:  N X Y Z

Arities: 

ar(0) = 0
ar(s) = 1
ar(posrecip) = 1
ar(negrecip) = 1
ar(nil) = 0
ar(cons) = 2
ar(cons2) = 2
ar(rnil) = 0
ar(rcons) = 2
ar(from) = 1
ar(2ndspos) = 2
ar(2ndsneg) = 2
ar(pi) = 1
ar(plus) = 2
ar(times) = 2
ar(square) = 1

Replacement map: 

µ(0) = {}
µ(s) = {1}
µ(posrecip) = {1}
µ(negrecip) = {1}
µ(nil) = {}
µ(cons) = {1}
µ(cons2) = {2}
µ(rnil) = {}
µ(rcons) = {1,2}
µ(from) = {1}
µ(2ndspos) = {1,2}
µ(2ndsneg) = {1,2}
µ(pi) = {1}
µ(plus) = {1,2}
µ(times) = {1,2}
µ(square) = {1}


Rules: (file ExAppendixB_AEL03)  

from(X) -> cons(X,from(s(X)))
2ndspos(0,Z) -> rnil
2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
2ndsneg(0,Z) -> rnil
2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
pi(X) -> 2ndspos(X,from(0))
plus(0,Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
times(0,Y) -> 0
times(s(X),Y) -> plus(Y,times(X,Y))
square(X) -> times(X,X)

The CS-TRS in OBJ format (file ExAppendixB_AEL03.obj):

obj ExAppendixB_AEL03 is
  sort S .
  op 0 : -> S .
  op s : S -> S .
  op posrecip : S -> S .
  op negrecip : S -> S .
  op nil : -> S .
  op cons : S S -> S [strat (1 0)] .
  op cons2 : S S -> S [strat (2 0)] .
  op rnil : -> S .
  op rcons : S S -> S .
  op from : S -> S .
  op 2ndspos : S S -> S .
  op 2ndsneg : S S -> S .
  op pi : S -> S .
  op plus : S S -> S .
  op times : S S -> S .
  op square : S -> S .
  vars N X Y Z : S .
  eq from(X) = cons(X,from(s(X))) .
  eq 2ndspos(0,Z) = rnil .
  eq 2ndspos(s(N),cons(X,Z)) = 2ndspos(s(N),cons2(X,Z)) .
  eq 2ndspos(s(N),cons2(X,cons(Y,Z))) = rcons(posrecip(Y),2ndsneg(N,Z)) .
  eq 2ndsneg(0,Z) = rnil .
  eq 2ndsneg(s(N),cons(X,Z)) = 2ndsneg(s(N),cons2(X,Z)) .
  eq 2ndsneg(s(N),cons2(X,cons(Y,Z))) = rcons(negrecip(Y),2ndspos(N,Z)) .
  eq pi(X) = 2ndspos(X,from(0)) .
  eq plus(0,Y) = Y .
  eq plus(s(X),Y) = s(plus(X,Y)) .
  eq times(0,Y) = 0 .
  eq times(s(X),Y) = plus(Y,times(X,Y)) .
  eq square(X) = times(X,X) .
endo

Negative results

1. The µ-termination of ExAppendixB_AEL03 cannot be proved by using Lucas' transformation: The TRS ExAppendixB_AEL03_L:

       from(X) -> cons(X)
       2ndspos(0,Z) -> rnil
       2ndspos(s(N),cons(X)) -> 2ndspos(s(N),cons2(Z))
       2ndspos(s(N),cons2(cons(Y))) -> rcons(posrecip(Y),2ndsneg(N,Z))
       2ndsneg(0,Z) -> rnil
       2ndsneg(s(N),cons(X)) -> 2ndsneg(s(N),cons2(Z))
       2ndsneg(s(N),cons2(cons(Y))) -> rcons(negrecip(Y),2ndspos(N,Z))
       pi(X) -> 2ndspos(X,from(0))
       plus(0,Y) -> Y
       plus(s(X),Y) -> s(plus(X,Y))
       times(0,Y) -> 0
       times(s(X),Y) -> plus(Y,times(X,Y))
       square(X) -> times(X,X)
       

   contains extra variables.

Positive results

1. The µ-termination of ExAppendixB_AEL03 can be proved by using Zantema's transformation. The TRS ExAppendixB_AEL03_Z:

        from(X) -> cons(X,n__from(s(X)))
        2ndspos(0,Z) -> rnil
        2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,activate(Z)))
        2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,activate(Z)))
        2ndsneg(0,Z) -> rnil
        2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,activate(Z)))
        2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,activate(Z)))
        pi(X) -> 2ndspos(X,from(0))
        plus(0,Y) -> Y
        plus(s(X),Y) -> s(plus(X,Y))
        times(0,Y) -> 0
        times(s(X),Y) -> plus(Y,times(X,Y))
        square(X) -> times(X,X)
        from(X) -> n__from(X)
        activate(n__from(X)) -> from(X)
        activate(X) -> X
        

   is terminating (use MetaCombination @ AProVE).
2. The µ-termination of ExAppendixB_AEL03 can also be proved by using Ferreira and Ribeiro's transformation. The TRS ExAppendixB_AEL03_FR:

        from(X) -> cons(X,n__from(n__s(X)))
        2ndspos(0,Z) -> rnil
        2ndspos(s(N),cons(X,n__cons(Y,Z))) -> rcons(posrecip(activate(Y)),2ndsneg(N,activate(Z)))
        2ndsneg(0,Z) -> rnil
        2ndsneg(s(N),cons(X,n__cons(Y,Z))) -> rcons(negrecip(activate(Y)),2ndspos(N,activate(Z)))
        pi(X) -> 2ndspos(X,from(0))
        plus(0,Y) -> Y
        plus(s(X),Y) -> s(plus(X,Y))
        times(0,Y) -> 0
        times(s(X),Y) -> plus(Y,times(X,Y))
        square(X) -> times(X,X)
        from(X) -> n__from(X)
        s(X) -> n__s(X)
        cons(X1,X2) -> n__cons(X1,X2)
        activate(n__from(X)) -> from(activate(X))
        activate(n__s(X)) -> s(activate(X))
        activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
        activate(X) -> X
        

   is terminating (use MetaCombination @ AProVE).
3. By [GM04, Theorem 22], the µ-termination of ExAppendixB_AEL03_GM can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).